tl;dr: this PR proposes separation logic-based implementation combinators for LowParse based on Pulse, the new separation logic language embedded in F*. This PR supersedes #54 .

Motivation

Coming up with a domain-specific language for formally verified parsing and serialization at the right level of abstraction with runtime efficiency in mind is much larger a research project than one may think, and we at Project Everest have been working on that for a very long time. Several challenges:

• minimize memory copies for speed ==> things must be serialized in the right order
• ease of user proof: how much layout details do we want to expose to the user
• inplace mutations and their impact on dependently parsed formats (e.g. tagged unions)
• must be extracted to (ideally auditable) C and Rust code

Our USENIX Security 2019 paper, particularly Sections 4.4 and 4.5, presents our first attempt in Low*, as done in miTLS, based on LowParse.Low.* validators and accessors. As described there, EverParse already produces such validators, accessors and serializer primitives for the user to write a Low* program reading and writing valid packets, and we extensively use them in miTLS and EverQuic, but layout details (e.g. offsets to the input/output buffers) are still very much exposed to the user.

This PR: Pulse+EverParse

In this PR, I propose to use Pulse, a separation logic framework for F*, to model resources for byte arrays containing byte representations valid with respect to a given parser specification: LowParse.Pulse.*

If a is a Pulse slice and s is a LowParse serializer specification, then LowParse.Pulse.Base.pts_to_serialized s a v says that a exactly contains bytes valid with respect to the parser p associated to s: p consumes all bytes of a and succeeds. Such a model seems to work with most parsers currently supported by LowParse, which either consume all their input or have the strong prefix property.

By using Pulse, the main goal is to hide most, if not all, offset reasoning away from the user.